#include <stdio.h>
#include <stdlib.h>
#include <iostream>
#include <fstream>
#include <vector>
#include <string.h>
//#include "cfa.h"
#include "smt.h"
#include "ARF.h"

using namespace std;

extern char *yytext;
extern FILE *yyin;
extern int yyparse(void);
extern vector<CFA> testcfa1();
extern vector<Prog*> fun;



int main(int argc, char** argv){

    CFA cfa;
    int i1;
    i1 = 0;
    //testyicesinterface();exit(0);// unit test for SMT
    //testpost1(art); exit(0);
    //testpost2(art); exit(0);
    //testpost3(art); exit(0);
    //testpost4(art); exit(0);
    //testwPre1(art); exit(0);
    //testwPre2(art); exit(0);
    //for catching: this is gcd function
    /*cfa1 = testcfa1();
    for(i1 = 0; i1 < cfa1.size(); i1++){
        cfa1[i1].CFA2Dot(argv[i1+1]);
    }
    exit(0);*/
    char infile[64];
    if(argc!=1){
    	strcpy(infile, argv[1]);
		yyin = fopen(argv[1], "r");
    }
    else{
    	cout<<"The file name of the testcase:";
    	cin>>infile;
    	//strcpy(infile, "testcase1.cc");
    }
	yyin = fopen(infile, "r");
	if(!yyin){
		cout<<"Error: There is no testcase \""<<infile<<"\"."<<endl<<"exit program!!"<<endl;
		exit(1);
	}
    yyparse();
    fclose(yyin);
    cout << "parsing the file!!!\n" << endl;

    vector<CFA> v_cfa;
    for(i1 = 0; i1 < (int)fun.size(); i1++){
        cfa.BuildGraph(i1);
        //cfa.PrintCFA();
        //cfa.CFA2Dot(argv[1],i1);
        cout<<"output file:"<<itoa(i1)<<endl;
        cfa.CFA2Dot((string(argv[1])+itoa(i1)+string(".dot")).c_str());

		v_cfa.push_back(cfa);
    }
    cout << "building the cfa!!!\n" << endl;

    //cfa.BuildCFA(*prog1);
    /*if(argc== 3 && strcmp(argv[2], "1") == 0){ cfa.PrintCFA(); }
    else if(argc== 3 && strcmp(argv[2], "2") == 0){ cfa.PrintBackCFA(); }
    else if(argc == 3){ cfa.CFA2Dot(argv[2]); }*/

    ARF arf(&v_cfa);
    cout<<"-------------------------------------GRAPH-------------------------------------"<<endl;
    arf.Graph_out("graph.dot");
    arf.Print_Summary_edge();
    cout<<"program done. No counterexample found."<<endl;

    return 0;
}

